poss:(ES{i}Prop{i'}), R:(possible-event{i:l}(poss)possible-event{i:l}(poss)Prop{i'}).
(Trans _1,_2:possible-event{i:l}(poss). R(_1,_2))
 (e1, e2:possible-event{i:l}(poss). poss-le{i:l}(e1; e2)  R(e1,e2))
 (P:(possible-event{i:l}(poss)Prop{i'}), e1, e2:possible-event{i:l}(poss).
 (poss-le{i:l}(e1; e2)  es-knows{i:l}(poss; R; P; e1)  es-knows{i:l}(poss; R; P; e2)) 

latex

Definitions	t  T, P  Q, x:A. B(x), f(a), Trans x,y:T. E(x;y), Type, Prop, ES, x:AB(x), PossibleEvent(poss), x,y. t(x;y), e1  e2, x:AB(x), K(P)@e
Lemmas	poss-le wf, trans wf, possible-event wf, event system wf